c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
↳ QTRS
↳ DependencyPairsProof
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
C(z, x, a) → F(z)
C(z, x, a) → B(f(z), z)
B(y, b(z, a)) → C(f(a), y, z)
B(y, b(z, a)) → F(a)
B(y, b(z, a)) → B(c(f(a), y, z), z)
C(z, x, a) → B(b(f(z), z), x)
B(y, b(z, a)) → F(b(c(f(a), y, z), z))
C(z, x, a) → F(b(b(f(z), z), x))
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
C(z, x, a) → F(z)
C(z, x, a) → B(f(z), z)
B(y, b(z, a)) → C(f(a), y, z)
B(y, b(z, a)) → F(a)
B(y, b(z, a)) → B(c(f(a), y, z), z)
C(z, x, a) → B(b(f(z), z), x)
B(y, b(z, a)) → F(b(c(f(a), y, z), z))
C(z, x, a) → F(b(b(f(z), z), x))
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
C(z, x, a) → B(f(z), z)
B(y, b(z, a)) → C(f(a), y, z)
B(y, b(z, a)) → B(c(f(a), y, z), z)
C(z, x, a) → B(b(f(z), z), x)
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
C(z, x, a) → B(f(z), z)
Used ordering: Polynomial interpretation [25,35]:
B(y, b(z, a)) → C(f(a), y, z)
B(y, b(z, a)) → B(c(f(a), y, z), z)
C(z, x, a) → B(b(f(z), z), x)
The value of delta used in the strict ordering is 1.
POL(C(x1, x2, x3)) = 2 + (1/2)x_1 + (1/4)x_2 + (1/4)x_3
POL(a) = 0
POL(f(x1)) = (1/2)x_1
POL(b(x1, x2)) = 4 + x_1
POL(c(x1, x2, x3)) = 4 + (2)x_1
POL(B(x1, x2)) = 1 + (1/4)x_1 + (1/4)x_2
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
B(y, b(z, a)) → C(f(a), y, z)
B(y, b(z, a)) → B(c(f(a), y, z), z)
C(z, x, a) → B(b(f(z), z), x)
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
B(y, b(z, a)) → C(f(a), y, z)
B(y, b(z, a)) → B(c(f(a), y, z), z)
Used ordering: Polynomial interpretation [25,35]:
C(z, x, a) → B(b(f(z), z), x)
The value of delta used in the strict ordering is 1/4.
POL(a) = 1/4
POL(C(x1, x2, x3)) = 4 + (4)x_1 + (4)x_2
POL(f(x1)) = (1/4)x_1
POL(b(x1, x2)) = 1/2 + (2)x_1 + (1/2)x_2
POL(c(x1, x2, x3)) = 1/4 + (3)x_1 + (1/4)x_2 + x_3
POL(B(x1, x2)) = 2 + (4)x_1 + (4)x_2
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
C(z, x, a) → B(b(f(z), z), x)
c(z, x, a) → f(b(b(f(z), z), x))
b(y, b(z, a)) → f(b(c(f(a), y, z), z))
f(c(c(z, a, a), x, a)) → z